The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z) [1]
g(true, x, y, z) → f(gt(x, z), x, s(y), z) [1]
g(true, x, y, z) → f(gt(x, z), x, y, s(z)) [1]
gt(0, v) → false [1]
gt(s(u), 0) → true [1]
gt(s(u), s(v)) → gt(u, v) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z) [1]
g(true, x, y, z) → f(gt(x, z), x, s(y), z) [1]
g(true, x, y, z) → f(gt(x, z), x, y, s(z)) [1]
gt(0, v) → false [1]
gt(s(u), 0) → true [1]
gt(s(u), s(v)) → gt(u, v) [1]

The TRS has the following type information:

f :: true:false → s:0 → s:0 → s:0 → f:g true :: true:false g :: true:false → s:0 → s:0 → s:0 → f:g gt :: s:0 → s:0 → true:false s :: s:0 → s:0 0 :: s:0 false :: true:false

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

f(v0, v1, v2, v3) → null_f [0]
g(v0, v1, v2, v3) → null_g [0]

And the following fresh constants:

null_f, null_g

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f(true, x, y, z) → g(gt(x, y), x, y, z) [1] g(true, x, y, z) → f(gt(x, z), x, s(y), z) [1] g(true, x, y, z) → f(gt(x, z), x, y, s(z)) [1] gt(0, v) → false [1] gt(s(u), 0) → true [1] gt(s(u), s(v)) → gt(u, v) [1] f(v0, v1, v2, v3) → null_f [0] g(v0, v1, v2, v3) → null_g [0] The TRS has the following type information: f :: true:false → s:0 → s:0 → s:0 → null_f:null_g true :: true:false g :: true:false → s:0 → s:0 → s:0 → null_f:null_g gt :: s:0 → s:0 → true:false s :: s:0 → s:0 0 :: s:0 false :: true:false null_f :: null_f:null_g null_g :: null_f:null_g Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

true => 1
0 => 0
false => 0
null_f => 0
null_g => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

f(z', z'', z1, z2) -{ 1 }→ g(gt(x, y), x, y, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
f(z', z'', z1, z2) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, v3 >= 0, z' = v0
g(z', z'', z1, z2) -{ 1 }→ f(gt(x, z), x, y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
g(z', z'', z1, z2) -{ 1 }→ f(gt(x, z), x, 1 + y, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
g(z', z'', z1, z2) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, v3 >= 0, z' = v0
gt(z', z'') -{ 1 }→ gt(u, v) :|: v >= 0, z' = 1 + u, z'' = 1 + v, u >= 0
gt(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 1 + u, u >= 0
gt(z', z'') -{ 1 }→ 0 :|: z'' = v, v >= 0, z' = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V3),0,[f(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[g(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[gt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(f(V, V1, V2, V3, Out),1,[gt(V4, V5, Ret0),g(Ret0, V4, V5, V6, Ret)],[Out = Ret,V2 = V5,V6 >= 0,V3 = V6,V4 >= 0,V5 >= 0,V1 = V4,V = 1]). eq(g(V, V1, V2, V3, Out),1,[gt(V7, V8, Ret01),f(Ret01, V7, 1 + V9, V8, Ret1)],[Out = Ret1,V2 = V9,V8 >= 0,V3 = V8,V7 >= 0,V9 >= 0,V1 = V7,V = 1]). eq(g(V, V1, V2, V3, Out),1,[gt(V10, V11, Ret02),f(Ret02, V10, V12, 1 + V11, Ret2)],[Out = Ret2,V2 = V12,V11 >= 0,V3 = V11,V10 >= 0,V12 >= 0,V1 = V10,V = 1]). eq(gt(V, V1, Out),1,[],[Out = 0,V1 = V13,V13 >= 0,V = 0]). eq(gt(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 1 + V14,V14 >= 0]). eq(gt(V, V1, Out),1,[gt(V15, V16, Ret3)],[Out = Ret3,V16 >= 0,V = 1 + V15,V1 = 1 + V16,V15 >= 0]). eq(f(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V17,V18 >= 0,V2 = V19,V20 >= 0,V1 = V20,V19 >= 0,V17 >= 0,V = V18]). eq(g(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V21,V22 >= 0,V2 = V23,V24 >= 0,V1 = V24,V23 >= 0,V21 >= 0,V = V22]). input_output_vars(f(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(g(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(gt(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [gt/3]
1. recursive : [f/5,g/5]
2. non_recursive : [start/4]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into gt/3
1. SCC is partially evaluated into g/5
2. SCC is partially evaluated into start/4

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations gt/3
* CE 8 is refined into CE [13]
* CE 7 is refined into CE [14]
* CE 6 is refined into CE [15]


### Cost equations --> "Loop" of gt/3
* CEs [14] --> Loop 8
* CEs [15] --> Loop 9
* CEs [13] --> Loop 10

### Ranking functions of CR gt(V,V1,Out)
* RF of phase [10]: [V,V1]

#### Partial ranking functions of CR gt(V,V1,Out)
* Partial RF of phase [10]:
- RF of loop [10:1]:
V
V1


### Specialization of cost equations g/5
* CE 9 is refined into CE [16,17,18,19]
* CE 12 is refined into CE [20]
* CE 10 is refined into CE [21,22,23,24,25,26]
* CE 11 is refined into CE [27,28,29,30]


### Cost equations --> "Loop" of g/5
* CEs [26] --> Loop 11
* CEs [30] --> Loop 12
* CEs [25] --> Loop 13
* CEs [29] --> Loop 14
* CEs [23] --> Loop 15
* CEs [28] --> Loop 16
* CEs [22] --> Loop 17
* CEs [27] --> Loop 18
* CEs [24] --> Loop 19
* CEs [21] --> Loop 20
* CEs [19] --> Loop 21
* CEs [18] --> Loop 22
* CEs [17] --> Loop 23
* CEs [16,20] --> Loop 24

### Ranking functions of CR g(V,V1,V2,V3,Out)
* RF of phase [11,12]: [2*V1-V2-V3-1]
* RF of phase [16]: [V1-V2-1]
* RF of phase [19]: [V1-V3]

#### Partial ranking functions of CR g(V,V1,V2,V3,Out)
* Partial RF of phase [11,12]:
- RF of loop [11:1]:
V1-V3
- RF of loop [12:1]:
V1-V2-1
* Partial RF of phase [16]:
- RF of loop [16:1]:
V1-V2-1
* Partial RF of phase [19]:
- RF of loop [19:1]:
V1-V3


### Specialization of cost equations start/4
* CE 2 is refined into CE [31]
* CE 3 is refined into CE [32,33,34,35,36,37,38,39,40]
* CE 4 is refined into CE [41,42,43,44]
* CE 5 is refined into CE [45,46,47,48]


### Cost equations --> "Loop" of start/4
* CEs [48] --> Loop 25
* CEs [42] --> Loop 26
* CEs [36] --> Loop 27
* CEs [44] --> Loop 28
* CEs [37,38,39,40,43,47] --> Loop 29
* CEs [31,33,34,35,41] --> Loop 30
* CEs [32,46] --> Loop 31
* CEs [45] --> Loop 32

### Ranking functions of CR start(V,V1,V2,V3)

#### Partial ranking functions of CR start(V,V1,V2,V3)


Computing Bounds
=====================================

#### Cost of chains of gt(V,V1,Out):
* Chain [[10],9]: 1*it(10)+1
Such that:it(10) =< V

with precondition: [Out=0,V>=1,V1>=V]

* Chain [[10],8]: 1*it(10)+1
Such that:it(10) =< V1

with precondition: [Out=1,V1>=1,V>=V1+1]

* Chain [9]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [8]: 1
with precondition: [V1=0,Out=1,V>=1]


#### Cost of chains of g(V,V1,V2,V3,Out):
* Chain [[19],[11,12],24]: 4*it(11)+4*it(12)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+2
Such that:it(11) =< V1-V3
aux(10) =< V1
aux(11) =< 2*V1-V3
it(12) =< aux(10)
it(19) =< aux(11)
it(11) =< aux(11)
it(12) =< aux(11)
aux(4) =< aux(10)-1
aux(3) =< aux(10)+1
s(9) =< it(11)*aux(10)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)
s(15) =< it(19)*aux(10)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [[19],[11,12],22]: 4*it(11)+4*it(12)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+1*s(16)+2
Such that:it(11) =< V1-V3
aux(14) =< V1
aux(15) =< 2*V1-V3
it(12) =< aux(14)
it(19) =< aux(15)
s(16) =< aux(14)
it(11) =< aux(15)
it(12) =< aux(15)
aux(4) =< aux(14)-1
aux(3) =< aux(14)+1
s(9) =< it(11)*aux(14)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)
s(15) =< it(19)*aux(14)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [[19],[11,12],21]: 4*it(11)+4*it(12)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+1*s(17)+2
Such that:it(11) =< V1-V3
aux(18) =< V1
aux(19) =< 2*V1-V3
it(12) =< aux(18)
it(19) =< aux(19)
s(17) =< aux(18)
it(11) =< aux(19)
it(12) =< aux(19)
aux(4) =< aux(18)-1
aux(3) =< aux(18)+1
s(9) =< it(11)*aux(18)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)
s(15) =< it(19)*aux(18)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [[19],[11,12],14,24]: 4*it(11)+4*it(12)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+2*s(18)+6
Such that:it(11) =< V1-V3
aux(22) =< V1
aux(23) =< 2*V1-V3
it(12) =< aux(22)
it(19) =< aux(23)
s(18) =< aux(22)
it(11) =< aux(23)
it(12) =< aux(23)
aux(4) =< aux(22)-1
aux(3) =< aux(22)+1
s(9) =< it(11)*aux(22)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)
s(15) =< it(19)*aux(22)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [[19],24]: 4*it(19)+1*s(15)+2
Such that:aux(9) =< V1
it(19) =< V1-V3
s(15) =< it(19)*aux(9)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+1]

* Chain [[19],22]: 4*it(19)+1*s(15)+1*s(16)+2
Such that:it(19) =< V1-V3
aux(24) =< V1
s(16) =< aux(24)
s(15) =< it(19)*aux(24)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+1]

* Chain [[19],21]: 4*it(19)+1*s(15)+1*s(17)+2
Such that:it(19) =< V1-V3
aux(25) =< V1
s(17) =< aux(25)
s(15) =< it(19)*aux(25)

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [[16],24]: 4*it(16)+1*s(22)+2
Such that:aux(26) =< V1
it(16) =< V1-V2
s(22) =< it(16)*aux(26)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],23]: 4*it(16)+1*s(22)+2
Such that:aux(26) =< V1
it(16) =< V1-V2
s(22) =< it(16)*aux(26)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],18,24]: 4*it(16)+1*s(22)+1*s(23)+6
Such that:it(16) =< V1-V2
aux(27) =< V1
s(23) =< aux(27)
s(22) =< it(16)*aux(27)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],15,[11,12],24]: 8*it(11)+4*it(16)+2*s(9)+1*s(11)+1*s(12)+1*s(22)+1*s(24)+6
Such that:aux(8) =< 2*V1
it(16) =< 2*V1-V2
aux(29) =< V1
it(11) =< aux(29)
s(24) =< aux(29)
it(11) =< aux(8)
aux(4) =< aux(29)-1
aux(3) =< aux(29)+1
s(9) =< it(11)*aux(29)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(22) =< it(16)*aux(29)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],15,[11,12],22]: 8*it(11)+4*it(16)+2*s(9)+1*s(11)+1*s(12)+2*s(16)+1*s(22)+6
Such that:aux(13) =< 2*V1
it(16) =< 2*V1-V2
aux(31) =< V1
it(11) =< aux(31)
s(16) =< aux(31)
it(11) =< aux(13)
aux(4) =< aux(31)-1
aux(3) =< aux(31)+1
s(9) =< it(11)*aux(31)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(22) =< it(16)*aux(31)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],15,[11,12],21]: 8*it(11)+4*it(16)+2*s(9)+1*s(11)+1*s(12)+2*s(17)+1*s(22)+6
Such that:aux(17) =< 2*V1
it(16) =< 2*V1-V2
aux(33) =< V1
it(11) =< aux(33)
s(17) =< aux(33)
it(11) =< aux(17)
aux(4) =< aux(33)-1
aux(3) =< aux(33)+1
s(9) =< it(11)*aux(33)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(22) =< it(16)*aux(33)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2,2*V1>=V2+5]

* Chain [[16],15,[11,12],14,24]: 8*it(11)+4*it(16)+2*s(9)+1*s(11)+1*s(12)+3*s(18)+1*s(22)+10
Such that:aux(21) =< 2*V1
it(16) =< 2*V1-V2
aux(35) =< V1
it(11) =< aux(35)
s(18) =< aux(35)
it(11) =< aux(21)
aux(4) =< aux(35)-1
aux(3) =< aux(35)+1
s(9) =< it(11)*aux(35)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(22) =< it(16)*aux(35)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2,2*V1>=V2+5]

* Chain [[16],15,24]: 4*it(16)+1*s(22)+1*s(24)+6
Such that:it(16) =< V1-V2
aux(36) =< V1
s(24) =< aux(36)
s(22) =< it(16)*aux(36)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],15,21]: 4*it(16)+1*s(17)+1*s(22)+1*s(24)+6
Such that:s(17) =< 1
it(16) =< V1-V2
aux(37) =< V1
s(24) =< aux(37)
s(22) =< it(16)*aux(37)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[16],15,14,24]: 4*it(16)+1*s(18)+2*s(19)+1*s(22)+10
Such that:s(18) =< 1
it(16) =< V1-V2
aux(38) =< V1
s(19) =< aux(38)
s(22) =< it(16)*aux(38)

with precondition: [V=1,V3=0,Out=0,V2>=0,V1>=V2+2]

* Chain [[11,12],24]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+2
Such that:aux(5) =< V1
it(12) =< V1-V2
it(11) =< V1-V3
aux(8) =< 2*V1-V2-V3
it(11) =< aux(8)
it(12) =< aux(8)
aux(4) =< aux(5)-1
aux(3) =< aux(5)+1
s(9) =< it(11)*aux(5)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+1,V1>=V3+1]

* Chain [[11,12],22]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+1*s(16)+2
Such that:it(12) =< V1-V2
it(11) =< V1-V3
aux(12) =< V1
aux(13) =< 2*V1-V2-V3
s(16) =< aux(12)
it(11) =< aux(13)
it(12) =< aux(13)
aux(4) =< aux(12)-1
aux(3) =< aux(12)+1
s(9) =< it(11)*aux(12)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+1,V1>=V3+1]

* Chain [[11,12],21]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+1*s(17)+2
Such that:it(12) =< V1-V2
it(11) =< V1-V3
aux(16) =< V1
aux(17) =< 2*V1-V2-V3
s(17) =< aux(16)
it(11) =< aux(17)
it(12) =< aux(17)
aux(4) =< aux(16)-1
aux(3) =< aux(16)+1
s(9) =< it(11)*aux(16)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+1,V1>=V3+1,2*V1>=V2+V3+3]

* Chain [[11,12],14,24]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+2*s(18)+6
Such that:it(12) =< V1-V2
it(11) =< V1-V3
aux(20) =< V1
aux(21) =< 2*V1-V2-V3
s(18) =< aux(20)
it(11) =< aux(21)
it(12) =< aux(21)
aux(4) =< aux(20)-1
aux(3) =< aux(20)+1
s(9) =< it(11)*aux(20)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+1,V1>=V3+1,2*V1>=V2+V3+3]

* Chain [24]: 2
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0]

* Chain [23]: 2
with precondition: [V=1,V3=0,Out=0,V1>=1,V2>=0]

* Chain [22]: 1*s(16)+2
Such that:s(16) =< V1

with precondition: [V=1,Out=0,V1>=1,V2>=0,V3>=V1]

* Chain [21]: 1*s(17)+2
Such that:s(17) =< V3

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V3+1]

* Chain [20,[19],[11,12],24]: 8*it(11)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+6
Such that:aux(11) =< 2*V1
aux(39) =< V1
it(11) =< aux(39)
it(19) =< aux(11)
it(11) =< aux(11)
aux(4) =< aux(39)-1
aux(3) =< aux(39)+1
s(9) =< it(11)*aux(39)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(15) =< it(19)*aux(39)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [20,[19],[11,12],22]: 8*it(11)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+1*s(16)+6
Such that:aux(15) =< 2*V1
aux(40) =< V1
it(11) =< aux(40)
it(19) =< aux(15)
s(16) =< aux(40)
it(11) =< aux(15)
aux(4) =< aux(40)-1
aux(3) =< aux(40)+1
s(9) =< it(11)*aux(40)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(15) =< it(19)*aux(40)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [20,[19],[11,12],21]: 8*it(11)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+1*s(17)+6
Such that:aux(19) =< 2*V1
aux(41) =< V1
it(11) =< aux(41)
it(19) =< aux(19)
s(17) =< aux(41)
it(11) =< aux(19)
aux(4) =< aux(41)-1
aux(3) =< aux(41)+1
s(9) =< it(11)*aux(41)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(15) =< it(19)*aux(41)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [20,[19],[11,12],14,24]: 8*it(11)+4*it(19)+2*s(9)+1*s(11)+1*s(12)+1*s(15)+2*s(18)+10
Such that:aux(23) =< 2*V1
aux(42) =< V1
it(11) =< aux(42)
it(19) =< aux(23)
s(18) =< aux(42)
it(11) =< aux(23)
aux(4) =< aux(42)-1
aux(3) =< aux(42)+1
s(9) =< it(11)*aux(42)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)
s(15) =< it(19)*aux(42)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [20,[19],24]: 4*it(19)+1*s(15)+6
Such that:aux(43) =< V1
it(19) =< aux(43)
s(15) =< it(19)*aux(43)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,[19],22]: 5*it(19)+1*s(15)+6
Such that:aux(44) =< V1
it(19) =< aux(44)
s(15) =< it(19)*aux(44)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,[19],21]: 5*it(19)+1*s(15)+6
Such that:aux(45) =< V1
it(19) =< aux(45)
s(15) =< it(19)*aux(45)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [20,[11,12],24]: 8*it(11)+2*s(9)+1*s(11)+1*s(12)+6
Such that:aux(8) =< 2*V1
aux(46) =< V1
it(11) =< aux(46)
it(11) =< aux(8)
aux(4) =< aux(46)-1
aux(3) =< aux(46)+1
s(9) =< it(11)*aux(46)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,[11,12],22]: 8*it(11)+2*s(9)+1*s(11)+1*s(12)+1*s(16)+6
Such that:aux(13) =< 2*V1
aux(47) =< V1
it(11) =< aux(47)
s(16) =< aux(47)
it(11) =< aux(13)
aux(4) =< aux(47)-1
aux(3) =< aux(47)+1
s(9) =< it(11)*aux(47)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,[11,12],21]: 8*it(11)+2*s(9)+1*s(11)+1*s(12)+1*s(17)+6
Such that:aux(17) =< 2*V1
aux(48) =< V1
it(11) =< aux(48)
s(17) =< aux(48)
it(11) =< aux(17)
aux(4) =< aux(48)-1
aux(3) =< aux(48)+1
s(9) =< it(11)*aux(48)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,[11,12],14,24]: 8*it(11)+2*s(9)+1*s(11)+1*s(12)+2*s(18)+10
Such that:aux(21) =< 2*V1
aux(49) =< V1
it(11) =< aux(49)
s(18) =< aux(49)
it(11) =< aux(21)
aux(4) =< aux(49)-1
aux(3) =< aux(49)+1
s(9) =< it(11)*aux(49)
s(11) =< it(11)*aux(4)
s(12) =< it(11)*aux(3)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [20,24]: 6
with precondition: [V=1,V2=0,V3=0,Out=0,V1>=1]

* Chain [20,22]: 1*s(16)+6
Such that:s(16) =< 1

with precondition: [V=1,V1=1,V2=0,V3=0,Out=0]

* Chain [20,21]: 1*s(17)+6
Such that:s(17) =< 1

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [18,24]: 1*s(23)+6
Such that:s(23) =< V1

with precondition: [V=1,V3=0,Out=0,V1>=1,V2+1>=V1]

* Chain [17,24]: 1*s(25)+6
Such that:s(25) =< V1

with precondition: [V=1,V3=0,Out=0,V1>=1,V2>=V1]

* Chain [15,[11,12],24]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+1*s(24)+6
Such that:it(12) =< V1-V2
aux(8) =< 2*V1-V2
s(24) =< V2
aux(28) =< V1
it(11) =< aux(28)
it(11) =< aux(8)
it(12) =< aux(8)
aux(4) =< aux(28)-1
aux(3) =< aux(28)+1
s(9) =< it(11)*aux(28)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [15,[11,12],22]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+1*s(16)+1*s(24)+6
Such that:it(12) =< V1-V2
aux(13) =< 2*V1-V2
s(24) =< V2
aux(30) =< V1
it(11) =< aux(30)
s(16) =< aux(30)
it(11) =< aux(13)
it(12) =< aux(13)
aux(4) =< aux(30)-1
aux(3) =< aux(30)+1
s(9) =< it(11)*aux(30)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [15,[11,12],21]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+1*s(17)+1*s(24)+6
Such that:it(12) =< V1-V2
aux(17) =< 2*V1-V2
s(24) =< V2
aux(32) =< V1
it(11) =< aux(32)
s(17) =< aux(32)
it(11) =< aux(17)
it(12) =< aux(17)
aux(4) =< aux(32)-1
aux(3) =< aux(32)+1
s(9) =< it(11)*aux(32)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1,2*V1>=V2+4]

* Chain [15,[11,12],14,24]: 4*it(11)+4*it(12)+2*s(9)+1*s(11)+1*s(12)+2*s(18)+1*s(24)+10
Such that:it(12) =< V1-V2
aux(21) =< 2*V1-V2
s(24) =< V2
aux(34) =< V1
it(11) =< aux(34)
s(18) =< aux(34)
it(11) =< aux(21)
it(12) =< aux(21)
aux(4) =< aux(34)-1
aux(3) =< aux(34)+1
s(9) =< it(11)*aux(34)
s(11) =< it(12)*aux(4)
s(12) =< it(12)*aux(3)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1,2*V1>=V2+4]

* Chain [15,24]: 1*s(24)+6
Such that:s(24) =< V2

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [15,21]: 1*s(17)+1*s(24)+6
Such that:s(17) =< 1
s(24) =< V2

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [15,14,24]: 1*s(18)+1*s(19)+1*s(24)+10
Such that:s(18) =< 1
s(24) =< V2
s(19) =< V2+1

with precondition: [V=1,V3=0,Out=0,V1=V2+1,V1>=2]

* Chain [14,24]: 1*s(18)+1*s(19)+6
Such that:s(19) =< V1
s(18) =< V3

with precondition: [V=1,Out=0,V3>=1,V2+1>=V1,V1>=V3+1]

* Chain [13,24]: 1*s(26)+1*s(27)+6
Such that:s(27) =< V1
s(26) =< V3+1

with precondition: [V=1,Out=0,V3>=1,V2>=V1,V1>=V3+1]


#### Cost of chains of start(V,V1,V2,V3):
* Chain [32]: 1
with precondition: [V=0,V1>=0]

* Chain [31]: 5*s(341)+56*s(343)+6*s(346)+4*s(354)+12
Such that:s(335) =< 1
aux(63) =< -V2
s(340) =< V2
s(341) =< s(335)
s(343) =< aux(63)
s(346) =< s(340)
s(351) =< 1
s(354) =< s(343)*s(351)

with precondition: [V1=0,V>=1]

* Chain [30]: 10*s(368)+119*s(369)+224*s(370)+48*s(372)+12*s(374)+56*s(379)+28*s(380)+28*s(381)+12*s(387)+1*s(389)+32*s(397)+32*s(398)+12*s(399)+2*s(401)+16*s(404)+8*s(405)+8*s(406)+3*s(407)+16*s(409)+4*s(413)+16*s(423)+24*s(424)+16*s(425)+6*s(426)+6*s(427)+16*s(429)+8*s(432)+4*s(433)+4*s(434)+4*s(441)+12
Such that:s(417) =< V1-V2
s(392) =< V1-V3
s(419) =< 2*V1-V2
aux(67) =< 2*V1-V3
s(420) =< V2
s(395) =< V3
s(389) =< V3+1
aux(68) =< 1
aux(69) =< V1
aux(70) =< 2*V1
s(369) =< aux(69)
s(368) =< aux(68)
s(370) =< aux(69)
s(372) =< aux(70)
s(374) =< s(369)*aux(69)
s(370) =< aux(70)
s(377) =< aux(69)-1
s(378) =< aux(69)+1
s(379) =< s(370)*aux(69)
s(380) =< s(370)*s(377)
s(381) =< s(370)*s(378)
s(387) =< s(372)*aux(69)
s(423) =< s(417)
s(424) =< s(417)
s(425) =< s(419)
s(426) =< s(420)
s(427) =< s(424)*aux(69)
s(429) =< aux(69)
s(429) =< s(419)
s(423) =< s(419)
s(432) =< s(429)*aux(69)
s(433) =< s(423)*s(377)
s(434) =< s(423)*s(378)
s(441) =< s(425)*aux(69)
s(397) =< aux(69)
s(398) =< s(392)
s(399) =< s(392)
s(401) =< s(395)
s(398) =< aux(67)
s(397) =< aux(67)
s(404) =< s(398)*aux(69)
s(405) =< s(397)*s(377)
s(406) =< s(397)*s(378)
s(407) =< s(399)*aux(69)
s(409) =< aux(67)
s(413) =< s(409)*aux(69)

with precondition: [V>=0,V1>=0,V2>=0,V3>=0]

* Chain [29]: 12*s(442)+7*s(449)+54*s(450)+16*s(451)+24*s(452)+16*s(453)+6*s(455)+3*s(456)+16*s(457)+8*s(460)+4*s(461)+4*s(462)+96*s(463)+24*s(464)+12*s(465)+12*s(466)+16*s(467)+4*s(468)+4*s(469)+1*s(471)+16*s(479)+16*s(480)+12*s(481)+16*s(482)+2*s(483)+8*s(486)+4*s(487)+4*s(488)+3*s(489)+16*s(490)+16*s(491)+8*s(492)+4*s(493)+4*s(494)+4*s(495)+2*s(499)+1*s(505)+12
Such that:s(505) =< V
s(474) =< V1-V3
s(446) =< 2*V1
s(447) =< 2*V1-V2
s(475) =< 2*V1-V2-V3
s(476) =< 2*V1-V3
s(477) =< V3
s(471) =< V3+1
aux(73) =< 1
aux(74) =< V1
aux(75) =< V1-V2
aux(76) =< V2
aux(77) =< V2+1
s(449) =< aux(73)
s(450) =< aux(74)
s(442) =< aux(76)
s(499) =< aux(77)
s(451) =< aux(75)
s(452) =< aux(75)
s(453) =< s(447)
s(455) =< s(452)*aux(74)
s(456) =< s(450)*aux(74)
s(457) =< aux(74)
s(457) =< s(447)
s(451) =< s(447)
s(458) =< aux(74)-1
s(459) =< aux(74)+1
s(460) =< s(457)*aux(74)
s(461) =< s(451)*s(458)
s(462) =< s(451)*s(459)
s(463) =< aux(74)
s(463) =< s(446)
s(464) =< s(463)*aux(74)
s(465) =< s(463)*s(458)
s(466) =< s(463)*s(459)
s(467) =< s(446)
s(468) =< s(467)*aux(74)
s(469) =< s(453)*aux(74)
s(479) =< aux(75)
s(480) =< s(474)
s(481) =< s(474)
s(482) =< s(474)
s(483) =< s(477)
s(480) =< s(475)
s(479) =< s(475)
s(486) =< s(480)*aux(74)
s(487) =< s(479)*s(458)
s(488) =< s(479)*s(459)
s(489) =< s(481)*aux(74)
s(490) =< aux(74)
s(491) =< s(476)
s(482) =< s(476)
s(490) =< s(476)
s(492) =< s(482)*aux(74)
s(493) =< s(490)*s(458)
s(494) =< s(490)*s(459)
s(495) =< s(491)*aux(74)

with precondition: [V>=1,V1>=V]

* Chain [28]: 1*s(506)+2
Such that:s(506) =< V1

with precondition: [V=1,V1>=1,V2>=0,V3>=V1]

* Chain [27]: 42*s(507)+5*s(514)+16*s(516)+24*s(517)+16*s(518)+6*s(519)+6*s(520)+3*s(521)+16*s(522)+8*s(525)+4*s(526)+4*s(527)+96*s(528)+24*s(529)+12*s(530)+12*s(531)+16*s(532)+4*s(533)+4*s(534)+12
Such that:s(508) =< 1
s(510) =< V1-V2
s(511) =< 2*V1
s(512) =< 2*V1-V2
s(513) =< V2
aux(78) =< V1
s(507) =< aux(78)
s(514) =< s(508)
s(516) =< s(510)
s(517) =< s(510)
s(518) =< s(512)
s(519) =< s(513)
s(520) =< s(517)*aux(78)
s(521) =< s(507)*aux(78)
s(522) =< aux(78)
s(522) =< s(512)
s(516) =< s(512)
s(523) =< aux(78)-1
s(524) =< aux(78)+1
s(525) =< s(522)*aux(78)
s(526) =< s(516)*s(523)
s(527) =< s(516)*s(524)
s(528) =< aux(78)
s(528) =< s(511)
s(529) =< s(528)*aux(78)
s(530) =< s(528)*s(523)
s(531) =< s(528)*s(524)
s(532) =< s(511)
s(533) =< s(532)*aux(78)
s(534) =< s(518)*aux(78)

with precondition: [V=1,V1>=1,V3>=0,V2>=V1]

* Chain [26]: 1*s(535)+12*s(542)+16*s(543)+16*s(544)+12*s(545)+16*s(546)+2*s(547)+8*s(550)+4*s(551)+4*s(552)+3*s(553)+16*s(554)+16*s(555)+8*s(556)+4*s(557)+4*s(558)+4*s(559)+6
Such that:s(536) =< V1
s(537) =< V1-V2
s(538) =< V1-V3
s(539) =< 2*V1-V2-V3
s(540) =< 2*V1-V3
s(541) =< V3
s(535) =< V3+1
s(542) =< s(536)
s(543) =< s(537)
s(544) =< s(538)
s(545) =< s(538)
s(546) =< s(538)
s(547) =< s(541)
s(544) =< s(539)
s(543) =< s(539)
s(548) =< s(536)-1
s(549) =< s(536)+1
s(550) =< s(544)*s(536)
s(551) =< s(543)*s(548)
s(552) =< s(543)*s(549)
s(553) =< s(545)*s(536)
s(554) =< s(536)
s(555) =< s(540)
s(546) =< s(540)
s(554) =< s(540)
s(556) =< s(546)*s(536)
s(557) =< s(554)*s(548)
s(558) =< s(554)*s(549)
s(559) =< s(555)*s(536)

with precondition: [V=1,V2>=0,V3>=1,V1>=V3+1]

* Chain [25]: 1*s(560)+1
Such that:s(560) =< V1

with precondition: [V1>=1,V>=V1+1]


Closed-form bounds of start(V,V1,V2,V3):
-------------------------------------
* Chain [32] with precondition: [V=0,V1>=0]
- Upper bound: 1
- Complexity: constant
* Chain [31] with precondition: [V1=0,V>=1]
- Upper bound: nat(V2)*6+17+nat(-V2)*60
- Complexity: n
* Chain [30] with precondition: [V>=0,V1>=0,V2>=0,V3>=0]
- Upper bound: 427*V1+22+112*V1*V1+12*V1* (2*V1)+10*V1*nat(V1-V2)+19*V1*nat(V1-V3)+4*V1*nat(2*V1-V2)+4*V1*nat(2*V1-V3)+6*V2+2*V3+nat(V1-1)*36*V1+nat(V1-1)*4*nat(V1-V2)+96*V1+ (V3+1)+nat(V1-V2)*44+nat(V1-V3)*44+nat(2*V1-V2)*16+nat(2*V1-V3)*16
- Complexity: n^2
* Chain [29] with precondition: [V>=1,V1>=V]
- Upper bound: V+198*V1+19+51*V1*V1+4*V1* (2*V1)+14*V1*nat(V1-V2)+19*V1*nat(V1-V3)+4*V1*nat(2*V1-V2)+4*V1*nat(2*V1-V3)+nat(V2)*12+nat(V3)*2+ (16*V1-16)*V1+ (8*V1-8)*nat(V1-V2)+32*V1+nat(V2+1)*2+nat(V3+1)+nat(V1-V2)*64+nat(V1-V3)*44+nat(2*V1-V2)*16+nat(2*V1-V3)*16
- Complexity: n^2
* Chain [28] with precondition: [V=1,V1>=1,V2>=0,V3>=V1]
- Upper bound: V1+2
- Complexity: n
* Chain [27] with precondition: [V=1,V1>=1,V3>=0,V2>=V1]
- Upper bound: 166*V1+17+47*V1*V1+4*V1* (2*V1)+4*V1*nat(2*V1-V2)+6*V2+ (12*V1-12)*V1+32*V1+nat(2*V1-V2)*16
- Complexity: n^2
* Chain [26] with precondition: [V=1,V2>=0,V3>=1,V1>=V3+1]
- Upper bound: 32*V1-16*V3+ (44*V1-44*V3+ (32*V1+6+4*V1*V1+4*V1*nat(V1-V2)+ (V1-V3)* (19*V1)+ (2*V1-V3)* (4*V1)+2*V3+ (4*V1-4)*V1+ (4*V1-4)*nat(V1-V2)+ (V3+1)+nat(V1-V2)*20))
- Complexity: n^2
* Chain [25] with precondition: [V1>=1,V>=V1+1]
- Upper bound: V1+1
- Complexity: n

### Maximum cost of start(V,V1,V2,V3): max([nat(V2)*6+16+nat(-V2)*60,31*V1+4+4*V1*V1+nat(V1-1)*4*V1+max([19*V1*nat(V1-V3)+4*V1*nat(V1-V2)+4*V1*nat(2*V1-V3)+nat(V3)*2+nat(V1-1)*4*nat(V1-V2)+nat(V3+1)+nat(V1-V2)*20+nat(V1-V3)*44+nat(2*V1-V3)*16,32*V1+2+4*V1*V1+10*V1*nat(V1-V2)+19*V1*nat(V1-V3)+4*V1*nat(2*V1-V3)+nat(V3)*2+nat(V1-1)*4*V1+nat(V1-1)*4*nat(V1-V2)+nat(V3+1)+nat(V1-V2)*44+nat(V1-V3)*44+nat(2*V1-V3)*16+max([229*V1+3+61*V1*V1+8*V1* (2*V1)+nat(V1-1)*20*V1+64*V1,4*V1*nat(V1-V2)+V+nat(V2)*6+nat(V1-1)*4*nat(V1-V2)+nat(V2+1)*2+nat(V1-V2)*20])+ (134*V1+11+43*V1*V1+4*V1* (2*V1)+4*V1*nat(2*V1-V2)+nat(V2)*6+nat(V1-1)*8*V1+32*V1+nat(2*V1-V2)*16)])+ (V1+1)])+1
Asymptotic class: n^2
* Total analysis performed in 1438 ms.

(10) BOUNDS(1, n^2)